module ApbPC
(
    input  [31:0] PRDATA,                             // APB read data
    input         PREADY,                             // APB ready signal
    input         PSLVERR,                            // APB error response
    input         PCLK,                               // APB Bus Clock
    input         PRESETn,                            // APB Reset
    input  [31:0] PADDR,                              // APB address
    input         PSEL,                               // APB select line
    input         PENABLE,                            // APB trans
    input         PWRITE,                             // APB Write
    input  [31:0] PWDATA                              // APB write data
);

  property APB_1;
    @(posedge PCLK) $rose(PSEL) |-> ##1 ($rose(PENABLE) && PSEL);
  endproperty
  apb_1: assert property (APB_1) else
   $error("AXI_ERRM_AWCACHE. When AWVALID is high, if AWCACHE[1] is low then AWCACHE[3] and AWCACHE[2] must also be low. Spec: table 5-1 on page 5-3.");

  property APB_2;
    @(posedge PCLK) $fell(PSEL) |-> (##0 $fell(PENABLE)) and ($past(PREADY,1) == 1'b1);
  endproperty
  apb_2: assert property (APB_2) else
   $error("AXI_ERRM_AWCACHE. When AWVALID is high, if AWCACHE[1] is low then AWCACHE[3] and AWCACHE[2] must also be low. Spec: table 5-1 on page 5-3.");
  
  property APB_3;
    @(posedge PCLK) PREADY && PENABLE && PSEL |-> ##1 ( $fell(PENABLE) && $fell(PSEL));
  endproperty
  apb_3: assert property (APB_3) else
   $error("AXI_ERRM_AWCACHE. When AWVALID is high, if AWCACHE[1] is low then AWCACHE[3] and AWCACHE[2] must also be low. Spec: table 5-1 on page 5-3.");

endmodule
